Search results for "first-order modal logic"

Unification in first-order transitive modal logic

2019

We introduce unification in first-order transitive modal logics, i.e. logics extending Q–K4, and apply it to solve some problems such as admissibility of rules. Unifiable formulas in some extensions of Q–K4 are characterized and an explicit basis for the passive rules (those with non-unifiable premises) is provided. Both unifiability and passive rules depend on the number of logical constants in the logic; we focus on extensions of Q–K4 with at most four constants ⊤,⊥,□⊥,◊⊤⁠. Projective formulas, defined in a way similar to propositional logic, are used to solve some questions concerning the disjunction and existence properties. A partial characterization of first-order modal logics with pr…